﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using System.Diagnostics.Contracts;

namespace TestGen
{
	public enum ConstraintType { Equality, LessEqual, GreaterEqual };

	/// <summary>
	/// This class is a simple way to define a constraint for use by our constraint solver/simplifer and for outputting into the constructor for
	/// later use.
	/// </summary>
	public sealed class TGenConstraint
	{
		private readonly ConstraintType m_ctype;
		private readonly TGenTerm m_t1;
		private readonly TGenTerm m_t2;

		public TGenConstraint(ConstraintType cty, TGenTerm t1, TGenTerm t2)
		{
			this.m_ctype = cty;
			this.m_t1 = t1;
			this.m_t2 = t2;
		}

		private static string OpTypeStr(ConstraintType ct)
		{
			String sws = null;
			switch(ct)
			{
				case ConstraintType.Equality:
					sws = "==";
					break;
				case ConstraintType.GreaterEqual:
					sws = ">=";
					break;
				case ConstraintType.LessEqual:
					sws = "<=";
					break;
			}
			return sws;
		}

		public override string ToString()
		{ return this.m_t1.ToString() + " " + OpTypeStr(this.m_ctype) + " " + this.m_t2.ToString(); }

		public string GenerateConstraintOutputForCSharp()
		{ return this.m_t1.GenerateTermOutputForCSharp() + " " + OpTypeStr(this.m_ctype) + " " + this.m_t2.GenerateTermOutputForCSharp(); }

		/// <summary>
		/// Var Remapping may have introduced constant expressions in the terms, simplify any constant terms.
		/// </summary>
		public TGenConstraint Simplify()
		{
			TGenTerm lt = this.m_t1.Simplify();
			TGenTerm rt = this.m_t2.Simplify();

			return new TGenConstraint(this.m_ctype, lt, rt);
		}


		public ConstraintType ConstraintOp { get { return this.m_ctype; } }
		public TGenTerm LeftTerm { get { return this.m_t1; } }
		public TGenTerm RightTerm { get { return this.m_t2; } }
	}

	/// <summary>
	/// This class is a simple way to define terms (vars, constants, and expressions) for use in the constraints.
	/// </summary>
	public abstract class TGenTerm
	{
		/// <summary>
		/// Replace terms with the new atomic terms as specified by the names in remap, return a new term with the remapping.
		/// </summary>
		public abstract TGenTerm TermRemap(Dictionary<TGenVar, TGenAtomTerm> remap);

		/// <summary>
		/// Var Remapping may have introduced constant expressions in the terms, simplify any constant terms.
		/// </summary>
		public abstract TGenTerm Simplify();

		/// <summary>
		/// Generate the Term for output in the csharp constructor.
		/// </summary>
		public abstract String GenerateTermOutputForCSharp();
	}

	/// <summary>
	/// This class is a simple way to define atomic terms (vars, constants) for use in the constraints.
	/// </summary>
	public abstract class TGenAtomTerm : TGenTerm, IEquatable<TGenAtomTerm>
	{
		/// <summary>
		/// Return a copy of the atomic term.
		/// </summary>
		public abstract TGenAtomTerm CopyAtomTerm();

		public abstract bool Equals(TGenAtomTerm other);

		public static int CompareAtomTerm(TGenAtomTerm t1, TGenAtomTerm t2)
		{
			Contract.Requires((t1 is TGenConst) | (t1 is TGenVar));
			Contract.Requires((t2 is TGenConst) | (t2 is TGenVar));

			if((t1 is TGenConst) && (t2 is TGenVar))
				return -1;
			else if((t1 is TGenVar) && (t2 is TGenConst))
				return 1;
			else if((t1 is TGenConst) && (t2 is TGenConst))
				return TGenConst.TGenConstCompare((TGenConst)t1, (TGenConst)t2);
			else
				return TGenVar.TGenVarCompare((TGenVar)t1, (TGenVar)t2);
		}
	}

	/// <summary>
	/// Simple Constant terms for integer values.
	/// </summary>
	public sealed class TGenConst : TGenAtomTerm
	{
		private readonly uint m_constval;

		public TGenConst(uint val)
		{ this.m_constval = val; }

		public override TGenAtomTerm CopyAtomTerm()
		{ return new TGenConst(this.m_constval); }

		public static int TGenConstCompare(TGenConst c1, TGenConst c2)
		{ return c1.m_constval.CompareTo(c2.m_constval); }

		public override string ToString()
		{ return this.m_constval.ToString(); }

		public override bool Equals(object obj)
		{ return (obj is TGenConst) && (this.m_constval == ((TGenConst)obj).m_constval); }

		public override bool Equals(TGenAtomTerm other)
		{ return (other is TGenConst) && (this.m_constval == ((TGenConst)other).m_constval); }

		public override int GetHashCode()
		{ return (int)this.m_constval; }

		public override TGenTerm TermRemap(Dictionary<TGenVar, TGenAtomTerm> remap)
		{ return this.CopyAtomTerm(); }

		public override TGenTerm Simplify()
		{ return this.CopyAtomTerm(); }

		public override string GenerateTermOutputForCSharp()
		{ return this.m_constval.ToString(); }

		public uint ConstVal { get { return this.m_constval; } }
	}

	public sealed class TGenVar : TGenAtomTerm
	{
		private readonly string m_name;

		public TGenVar(string name)
		{ this.m_name = name; }

		public override TGenAtomTerm CopyAtomTerm()
		{ return new TGenVar(this.m_name); }

		public static int TGenVarCompare(TGenVar v1, TGenVar v2)
		{ return v1.m_name.CompareTo(v2.m_name); }

		public override string ToString()
		{ return this.m_name; }

		public override bool Equals(object obj)
		{ return (obj is TGenVar) && ((TGenVar)obj).m_name.Equals(this.m_name); }

		public override bool Equals(TGenAtomTerm other)
		{ return (other is TGenVar) && ((TGenVar)other).m_name.Equals(this.m_name); }

		public override int GetHashCode()
		{ return this.m_name.GetHashCode(); }

		public override TGenTerm TermRemap(Dictionary<TGenVar, TGenAtomTerm> remap)
		{ return (remap.ContainsKey(this) ? remap[this].CopyAtomTerm() : this.CopyAtomTerm()); }

		public override TGenTerm Simplify()
		{ return this.CopyAtomTerm(); }

		public override String GenerateTermOutputForCSharp()
		{ return this.m_name; }

		public String VarName { get { return this.m_name; } }
	}

	public sealed class TGenBinMult : TGenTerm
	{
		private readonly TGenTerm m_t1;
		private readonly TGenTerm m_t2;

		public TGenBinMult(TGenTerm t1, TGenTerm t2)
		{
			this.m_t1 = t1;
			this.m_t2 = t2;
		}

		public override string ToString()
		{ return "(" + this.m_t1.ToString() + " * " + this.m_t2.ToString() + ")"; }

		public override TGenTerm TermRemap(Dictionary<TGenVar, TGenAtomTerm> remap)
		{
			TGenTerm nt1 = this.m_t1.TermRemap(remap);
			TGenTerm nt2 = this.m_t2.TermRemap(remap);

			return new TGenBinMult(nt1, nt2);
		}

		public override TGenTerm Simplify()
		{
			TGenTerm nt1 = this.m_t1.Simplify();
			TGenTerm nt2 = this.m_t2.Simplify();

			if((nt1 is TGenConst) && (nt2 is TGenConst))
				return new TGenConst(((TGenConst)nt1).ConstVal * ((TGenConst)nt2).ConstVal);
			else
				return new TGenBinMult(nt1, nt2);
		}

		public override string GenerateTermOutputForCSharp()
		{ return "(" + this.m_t1.GenerateTermOutputForCSharp() + " * " + this.m_t2.GenerateTermOutputForCSharp() + ")"; }

		public TGenTerm Val1 { get { return this.m_t1; } }
		public TGenTerm Val2 { get { return this.m_t2; } }
	}

	public sealed class TGenSum : TGenTerm
	{
		private readonly TGenTerm[] m_sigmavals;

		public TGenSum(TGenTerm[] sigmavals)
		{
			this.m_sigmavals = new TGenTerm[sigmavals.Length];
			sigmavals.CopyTo(this.m_sigmavals, 0);
			this.OrganizeTermsNicely();
		}

		public TGenSum(TGenTerm t1, TGenTerm t2)
		{
			this.m_sigmavals = new TGenTerm[2];
			this.m_sigmavals[0] = t1;
			this.m_sigmavals[1] = t2;
			this.OrganizeTermsNicely();
		}

		private void OrganizeTermsNicely()
		{
			List<TGenConst> cl = new List<TGenConst>();
			List<TGenVar> vl = new List<TGenVar>();
			List<TGenBinMult> ml = new List<TGenBinMult>();
			List<TGenSum> sl = new List<TGenSum>();

			foreach(TGenTerm t in this.m_sigmavals)
			{
				if(t is TGenConst)
					cl.Add((TGenConst)t);
				else if(t is TGenVar)
					vl.Add((TGenVar)t);
				else if(t is TGenBinMult)
					ml.Add((TGenBinMult)t);
				else if(t is TGenSum)
					sl.Add((TGenSum)t);
				else
					throw new ArgumentException("Unknown TGenTerm Type Found!!");
			}

			List<TGenTerm> rl = new List<TGenTerm>();
			rl.AddRange(sl);
			rl.AddRange(ml);
			vl.Sort(TGenVar.TGenVarCompare);
			rl.AddRange(vl);
			cl.Sort(TGenConst.TGenConstCompare);
			rl.AddRange(cl);

			Array.Clear(this.m_sigmavals, 0, this.m_sigmavals.Length);
			rl.CopyTo(this.m_sigmavals);
		}

		public override string ToString()
		{
			if(this.m_sigmavals.Length == 0)
				return "sigma-0";
			else if(this.m_sigmavals.Length == 1)
				return "sigma-" + this.m_sigmavals[0].ToString();
			else
			{
				StringBuilder sb = new StringBuilder("(");
				for(int i = 0; i < this.m_sigmavals.Length; ++i)
				{
					if(i != 0) sb.Append(" + ");
					sb.Append(this.m_sigmavals[i].ToString());
				}
				sb.Append(")");

				return sb.ToString();
			}
		}

		public override TGenTerm TermRemap(Dictionary<TGenVar, TGenAtomTerm> remap)
		{
			TGenTerm[] rra = new TGenTerm[this.m_sigmavals.Length];
			for(int i = 0; i < this.m_sigmavals.Length; ++i)
			{
				TGenTerm t = this.m_sigmavals[i].TermRemap(remap);
				rra[i] = t;
			}

			return new TGenSum(rra);
		}

		public override TGenTerm Simplify()
		{
			//simplify any sub-terms and flatten any nested sums
			List<TGenTerm> flatl = new List<TGenTerm>();
			foreach(TGenTerm t in this.m_sigmavals)
			{
				TGenTerm nt = t.Simplify();
				if(nt is TGenSum)
					flatl.AddRange(((TGenSum)nt).m_sigmavals);
				else
					flatl.Add(nt);
			}

			//partition into list of multiplication, consts, and vars
			List<TGenBinMult> multl = new List<TGenBinMult>();
			List<TGenVar> varl = new List<TGenVar>();
			List<TGenConst> constl = new List<TGenConst>();

			foreach(TGenTerm t in flatl)
			{
				Contract.Assert(!(t is TGenSum), "Should be flattned??");

				if(t is TGenConst)
					constl.Add((TGenConst)t);
				else if(t is TGenVar)
					varl.Add((TGenVar)t);
				else
					multl.Add((TGenBinMult)t);
			}

			List<TGenTerm> finalterms = new List<TGenTerm>();
			//now do the constant sums and turn any multiple variable appearances into constant multiples while loading the final list for the simplified result
			if(constl.Count != 0)
			{
				uint csum = constl.Aggregate((uint)0, (uint acc, TGenConst cv) => acc + cv.ConstVal);
				finalterms.Add(new TGenConst(csum));
			}

			while(varl.Count != 0)
			{
				TGenVar cv = varl[0];
				uint count = (uint)varl.Count((TGenVar ov) => cv.Equals(ov));
				if(count == 1)
					finalterms.Add(cv);
				else
					finalterms.Add(new TGenBinMult(new TGenConst(count), cv));

				varl.RemoveAll((TGenVar ov) => cv.Equals(ov));
			}

			finalterms.AddRange(multl);

			//check on the cardinality and produce the final value
			if(finalterms.Count == 0)
				return new TGenConst(0);
			else if(finalterms.Count == 1)
				return finalterms[0];
			else
			{
				TGenTerm[] tga = finalterms.ToArray();
				return new TGenSum(tga);
			}
		}

		public override string GenerateTermOutputForCSharp()
		{
			Contract.Assert(this.m_sigmavals.Length >= 2, "Should be simplified eariler");

			StringBuilder sb = new StringBuilder("(");
			for(int i = 0; i < this.m_sigmavals.Length; ++i)
			{
				if(i != 0) sb.Append(" + ");
				sb.Append(this.m_sigmavals[i].GenerateTermOutputForCSharp());
			}
			sb.Append(")");

			return sb.ToString();
		}

		public TGenTerm[] SumTerms { get { return this.m_sigmavals; } }
	}
}
